Problem:
 2(7(x1)) -> 1(8(x1))
 2(8(1(x1))) -> 8(x1)
 2(8(x1)) -> 4(x1)
 5(9(x1)) -> 0(x1)
 4(x1) -> 5(2(3(x1)))
 5(3(x1)) -> 6(0(x1))
 2(8(x1)) -> 7(x1)
 4(7(x1)) -> 1(3(x1))
 5(2(6(x1))) -> 6(2(4(x1)))
 9(7(x1)) -> 7(5(x1))
 7(2(x1)) -> 4(x1)
 7(0(x1)) -> 9(3(x1))
 6(9(x1)) -> 9(x1)
 9(5(9(x1))) -> 5(7(x1))
 4(x1) -> 9(6(6(x1)))
 9(x1) -> 6(7(x1))
 6(2(x1)) -> 7(7(x1))
 2(4(x1)) -> 0(7(x1))
 6(6(x1)) -> 3(x1)
 0(3(x1)) -> 5(3(x1))

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {10,9,8,7,6,5,4}
   transitions:
    51(111) -> 112*
    51(41) -> 42*
    51(113) -> 114*
    51(105) -> 106*
    31(49) -> 50*
    31(39) -> 40*
    31(43) -> 44*
    61(97) -> 98*
    61(87) -> 88*
    61(77) -> 78*
    61(52) -> 53*
    61(89) -> 90*
    61(103) -> 104*
    61(78) -> 79*
    61(95) -> 96*
    71(75) -> 76*
    71(67) -> 68*
    71(69) -> 70*
    91(79) -> 80*
    01(59) -> 60*
    01(61) -> 62*
    01(51) -> 52*
    21(40) -> 41*
    41(29) -> 30*
    41(31) -> 32*
    41(23) -> 24*
    81(15) -> 16*
    81(21) -> 22*
    81(13) -> 14*
    32(177) -> 178*
    32(121) -> 122*
    32(183) -> 184*
    32(205) -> 206*
    32(185) -> 186*
    32(135) -> 136*
    32(125) -> 126*
    62(172) -> 173*
    62(167) -> 168*
    62(152) -> 153*
    62(164) -> 165*
    62(151) -> 152*
    62(141) -> 142*
    62(163) -> 164*
    20(2) -> 4*
    20(1) -> 4*
    20(3) -> 4*
    72(171) -> 172*
    70(2) -> 8*
    70(1) -> 8*
    70(3) -> 8*
    92(153) -> 154*
    92(165) -> 166*
    10(2) -> 1*
    10(1) -> 1*
    10(3) -> 1*
    02(149) -> 150*
    02(143) -> 144*
    02(140) -> 141*
    80(2) -> 2*
    80(1) -> 2*
    80(3) -> 2*
    52(127) -> 128*
    52(123) -> 124*
    40(2) -> 6*
    40(1) -> 6*
    40(3) -> 6*
    22(122) -> 123*
    22(126) -> 127*
    50(2) -> 5*
    50(1) -> 5*
    50(3) -> 5*
    33(217) -> 218*
    33(209) -> 210*
    33(203) -> 204*
    33(215) -> 216*
    90(2) -> 7*
    90(1) -> 7*
    90(3) -> 7*
    63(196) -> 197*
    63(193) -> 194*
    00(2) -> 10*
    00(1) -> 10*
    00(3) -> 10*
    73(192) -> 193*
    73(195) -> 196*
    30(2) -> 3*
    30(1) -> 3*
    30(3) -> 3*
    60(2) -> 9*
    60(1) -> 9*
    60(3) -> 9*
    1 -> 87,69,59,43,29,15
    2 -> 89,67,51,49,23,13
    3 -> 77,75,61,39,31,21
    14 -> 4*
    16 -> 4*
    22 -> 4*
    23 -> 163,125
    24 -> 4*
    29 -> 167,135
    30 -> 4*
    31 -> 151,121
    32 -> 4*
    39 -> 143*
    40 -> 113*
    42 -> 6*
    43 -> 149*
    44 -> 111,40
    49 -> 140*
    50 -> 105,40
    53 -> 5*
    60 -> 52*
    62 -> 52*
    68 -> 103,4
    70 -> 97,4
    76 -> 95,4
    77 -> 183*
    79 -> 171*
    80 -> 6*
    87 -> 177*
    88 -> 78*
    89 -> 185*
    90 -> 78*
    96 -> 7*
    98 -> 7*
    104 -> 7*
    106 -> 144,141,62,52,10
    112 -> 144,141,62,52,10
    114 -> 144,141,62,52,10
    124 -> 30,32
    128 -> 24*
    136 -> 122*
    141 -> 217,205
    142 -> 112,106,114
    144 -> 141*
    150 -> 141*
    151 -> 215*
    153 -> 192*
    154 -> 30,32
    163 -> 203*
    165 -> 195*
    166 -> 24*
    167 -> 209*
    168 -> 152*
    173 -> 80,6
    178 -> 79*
    184 -> 79*
    186 -> 79*
    194 -> 154,32,30
    197 -> 166*
    204 -> 165*
    206 -> 53,5
    210 -> 153*
    216 -> 153*
    218 -> 142*
  problem:
   
  Qed